YES 33.558 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((lookup :: Float  ->  [(Float,a)]  ->  Maybe a) :: Float  ->  [(Float,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((lookup :: Float  ->  [(Float,a)]  ->  Maybe a) :: Float  ->  [(Float,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
lookup k [] = Nothing
lookup k ((x,y: xys)
 | k == x
 = Just y
 | otherwise
 = lookup k xys

is transformed to
lookup k [] = lookup3 k []
lookup k ((x,y: xys) = lookup2 k ((x,y: xys)

lookup1 k x y xys True = Just y
lookup1 k x y xys False = lookup0 k x y xys otherwise

lookup0 k x y xys True = lookup k xys

lookup2 k ((x,y: xys) = lookup1 k x y xys (k == x)

lookup3 k [] = Nothing
lookup3 ww wx = lookup2 ww wx



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (lookup :: Float  ->  [(Float,a)]  ->  Maybe a)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wy6200), Succ(wy4000000)) → new_primPlusNat(wy6200, wy4000000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(wy30000), wy400000) → new_primMulNat(wy30000, wy400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup1121(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy2680), be) → new_lookup1127(wy44, Succ(wy4500), wy46, Succ(wy4700), wy48, wy49, be)
new_lookup135(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy1510), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup164(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1105(wy29, wy3000, wy31, wy3200, wy33, wy34, Zero, Succ(Succ(wy17100)), bc) → new_lookup1114(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup1117(wy44, wy4500, wy46, wy4700, wy48, wy49, Zero, Succ(Succ(wy26000)), be) → new_lookup1126(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup137(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1104(wy29, wy3000, wy31, wy3200, wy33, wy34, Zero, Succ(Succ(wy16900)), bc) → new_lookup1112(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup1141(wy17, wy18, wy19, Succ(wy4080), bg) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wy19, bg)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup151(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup199(wy400100, wy401, wy41, Succ(wy3830), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup199(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Zero))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup1106(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy1730), bc) → new_lookup1110(wy29, Succ(wy3000), wy31, Succ(wy3200), wy33, wy34, bc)
new_lookup1104(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy13800), Succ(Zero), bc) → new_lookup1112(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup132(wy29, Neg(wy300), wy31, Neg(wy320), wy33, wy34, Succ(wy1380), bc) → new_lookup(Float(Pos(Succ(wy29)), Neg(wy300)), wy34, bc)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup184(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup156(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup1100(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup111(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup132(wy29, Pos(Succ(wy3000)), wy31, Pos(Succ(wy3200)), wy33, wy34, Zero, bc) → new_lookup1106(wy29, wy3000, wy31, wy3200, wy33, wy34, new_primPlusNat0(new_primMulNat0(wy3000, wy3200), Succ(wy3200)), bc)
new_lookup190(wy3000, wy400100, wy401, wy41, Succ(wy3470), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup170(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy2820), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup1130(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy3530), bf) → new_lookup1135(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup177(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup132(wy29, Pos(Succ(wy3000)), wy31, Neg(Succ(wy3200)), wy33, wy34, Succ(wy1380), bc) → new_lookup1104(wy29, wy3000, wy31, wy3200, wy33, wy34, wy1380, new_primPlusNat0(new_primMulNat0(wy3000, wy3200), Succ(wy3200)), bc)
new_lookup182(wy51, Neg(Succ(wy5200)), wy53, Neg(Succ(wy5400)), wy55, wy56, Succ(wy3180), bf) → new_lookup1129(wy51, wy5200, wy53, wy5400, wy55, wy56, wy3180, new_primPlusNat0(new_primMulNat0(wy5200, wy5400), Succ(wy5400)), bf)
new_lookup118(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy840), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup1114(wy29, wy3000, wy31, wy3200, wy33, wy34, bc) → new_lookup0(Float(Pos(Succ(wy29)), Neg(Succ(wy3000))), wy31, wy3200, wy33, wy34, bc)
new_lookup1145(wy22, wy2300, wy24, wy2500, wy26, wy27, ba) → new_lookup(Float(Pos(Succ(wy22)), Neg(Succ(wy2300))), wy27, ba)
new_lookup132(wy29, Pos(Succ(wy3000)), wy31, Neg(Succ(wy3200)), wy33, wy34, Zero, bc) → new_lookup1107(wy29, wy3000, wy31, wy3200, wy33, wy34, new_primPlusNat0(new_primMulNat0(wy3000, wy3200), Succ(wy3200)), bc)
new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup1118(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy2620), be) → new_lookup1122(wy44, Succ(wy4500), wy46, Succ(wy4700), wy48, wy49, be)
new_lookup1111(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy13800), Succ(wy16900), bc) → new_lookup1111(wy29, wy3000, wy31, wy3200, wy33, wy34, wy13800, wy16900, bc)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup169(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup143(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup157(wy44, Pos(Succ(wy4500)), wy46, Neg(Succ(wy4700)), wy48, wy49, Succ(wy2290), be) → new_lookup1116(wy44, wy4500, wy46, wy4700, wy48, wy49, wy2290, new_primPlusNat0(new_primMulNat0(wy4500, wy4700), Succ(wy4700)), be)
new_lookup1100(wy310000, wy400100, wy401, wy41, Succ(wy3850), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup180(wy310000, wy400100, wy401, wy41, Succ(wy3120), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup1111(wy29, wy3000, wy31, wy3200, wy33, wy34, Zero, Succ(wy16900), bc) → new_lookup1112(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup1111(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy13800), Zero, bc) → new_lookup1112(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup197(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1139(wy51, wy5200, wy53, wy5400, wy55, wy56, bf) → new_lookup(Float(Neg(Succ(wy51)), Neg(Succ(wy5200))), wy56, bf)
new_lookup160(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy2400), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup151(wy310000, wy400100, wy401, wy41, Succ(wy2110), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup1102(wy310000, wy400100, wy401, wy41, Succ(wy3910), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup180(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup182(wy51, Pos(Succ(wy5200)), wy53, Pos(Succ(wy5400)), wy55, wy56, Succ(wy3180), bf) → new_lookup1128(wy51, wy5200, wy53, wy5400, wy55, wy56, wy3180, new_primPlusNat0(new_primMulNat0(wy5200, wy5400), Succ(wy5400)), bf)
new_lookup132(wy29, Pos(Zero), wy31, Neg(Zero), wy33, wy34, Succ(wy1380), bc) → new_lookup(Float(Pos(Succ(wy29)), Pos(Zero)), wy34, bc)
new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup133(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup147(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy1990), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup185(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy3310), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup192(wy400000, wy400100, wy401, wy41, Succ(wy3650), bb) → new_lookup0(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wy400000, wy400100, wy401, wy41, bb)
new_lookup157(wy44, Neg(Succ(wy4500)), wy46, Pos(Succ(wy4700)), wy48, wy49, Succ(wy2290), be) → new_lookup1117(wy44, wy4500, wy46, wy4700, wy48, wy49, wy2290, new_primPlusNat0(new_primMulNat0(wy4500, wy4700), Succ(wy4700)), be)
new_lookup1129(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy31800), Succ(Zero), bf) → new_lookup1139(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup1(wy22, Pos(Succ(wy2300)), wy24, Pos(Zero), wy26, wy27, Succ(wy630), ba) → new_lookup(Float(Pos(Succ(wy22)), Pos(Succ(wy2300))), wy27, ba)
new_lookup1120(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy2660), be) → new_lookup1126(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup1(wy22, Neg(Succ(wy2300)), wy24, Neg(Succ(wy2500)), wy26, wy27, Zero, ba) → new_lookup15(wy22, wy2300, wy24, wy2500, wy26, wy27, new_primPlusNat0(new_primMulNat0(wy2300, wy2500), Succ(wy2500)), ba)
new_lookup162(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy2460), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(wy31000)))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup193(wy31000, Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401, wy41, wy400100, bb)
new_lookup13(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy940), ba) → new_lookup1142(wy22, Succ(wy2300), wy24, Succ(wy2500), wy26, wy27, ba)
new_lookup126(wy310000, wy400100, wy401, wy41, Succ(wy1200), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), wy31), :(@2(Float(Neg(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup132(wy3000, wy31, wy400000, wy4001, wy401, wy41, new_primPlusNat0(new_primMulNat0(wy3000, wy400000), Succ(wy400000)), bb)
new_lookup182(wy51, Neg(Zero), wy53, Neg(Zero), wy55, wy56, Succ(wy3180), bf) → new_lookup(Float(Neg(Succ(wy51)), Neg(Zero)), wy56, bf)
new_lookup1131(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy3550), bf) → new_lookup1136(wy51, Succ(wy5200), wy53, Succ(wy5400), wy55, wy56, bf)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup125(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Zero))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup122(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Zero))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Zero))), wy41, bb)
new_lookup181(wy400100, wy401, wy41, Succ(wy3160), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup149(wy310000, wy400100, wy401, wy41, Succ(wy2050), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup178(wy310000, wy400100, wy401, wy41, Succ(wy3060), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup182(wy51, Neg(Succ(wy5200)), wy53, Pos(Succ(wy5400)), wy55, wy56, Zero, bf) → new_lookup1132(wy51, wy5200, wy53, wy5400, wy55, wy56, new_primPlusNat0(new_primMulNat0(wy5200, wy5400), Succ(wy5400)), bf)
new_lookup1(wy22, Pos(Zero), wy24, Pos(Succ(wy2500)), wy26, wy27, Succ(wy630), ba) → new_lookup(Float(Pos(Succ(wy22)), Pos(Zero)), wy27, ba)
new_lookup122(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy1080), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup1116(wy44, wy4500, wy46, wy4700, wy48, wy49, Zero, Succ(Succ(wy25800)), be) → new_lookup1124(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup171(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup143(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy1870), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup123(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup159(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup187(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy3370), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup161(wy3000, wy400100, wy401, wy41, Succ(wy2440), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup111(wy3000, wy400100, wy401, wy41, Succ(wy640), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup121(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup187(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1137(wy51, wy520, wy53, wy540, wy55, wy56, bf) → new_lookup(Float(Neg(Succ(wy51)), Neg(wy520)), wy56, bf)
new_lookup11(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy6300), Succ(Zero), ba) → new_lookup1145(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup1142(wy22, wy230, wy24, wy250, wy26, wy27, ba) → new_lookup(Float(Pos(Succ(wy22)), Pos(wy230)), wy27, ba)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup175(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1116(wy44, wy4500, wy46, wy4700, wy48, wy49, wy2290, Zero, be) → new_lookup(Float(Neg(Succ(wy44)), Pos(Succ(wy4500))), wy49, be)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup183(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup186(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup136(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup182(wy51, Pos(Zero), wy53, Pos(Zero), wy55, wy56, Succ(wy3180), bf) → new_lookup(Float(Neg(Succ(wy51)), Pos(Zero)), wy56, bf)
new_lookup156(wy400100, wy401, wy41, Succ(wy2270), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup1144(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy6300), Succ(wy9000), ba) → new_lookup1144(wy22, wy2300, wy24, wy2500, wy26, wy27, wy6300, wy9000, ba)
new_lookup1(wy22, Pos(wy230), wy24, Neg(wy250), wy26, wy27, Succ(wy630), ba) → new_lookup(Float(Pos(Succ(wy22)), Pos(wy230)), wy27, ba)
new_lookup157(wy44, Pos(Zero), wy46, Neg(Succ(wy4700)), wy48, wy49, Succ(wy2290), be) → new_lookup(Float(Neg(Succ(wy44)), Pos(Zero)), wy49, be)
new_lookup1138(wy51, wy5200, wy53, wy5400, wy55, wy56, Zero, Succ(wy35100), bf) → new_lookup1139(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup1138(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy31800), Zero, bf) → new_lookup1139(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup196(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup127(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup119(wy400000, wy400100, wy401, wy41, Succ(wy1000), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup128(wy310000, wy400100, wy401, wy41, Succ(wy1260), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup189(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1101(wy400100, wy401, wy41, Succ(wy3890), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Zero))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Zero))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup162(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1140(wy160, wy17, wy18, wy19, Succ(wy4040), bg) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy160))))), wy19, bg)
new_lookup15(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy980), ba) → new_lookup1145(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup152(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup157(wy44, Neg(Zero), wy46, Pos(Succ(wy4700)), wy48, wy49, Succ(wy2290), be) → new_lookup(Float(Neg(Succ(wy44)), Neg(Zero)), wy49, be)
new_lookup169(wy400000, wy400100, wy401, wy41, Succ(wy2800), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup1125(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy22900), Succ(wy26000), be) → new_lookup1125(wy44, wy4500, wy46, wy4700, wy48, wy49, wy22900, wy26000, be)
new_lookup157(wy44, Pos(wy450), wy46, Pos(wy470), wy48, wy49, Succ(wy2290), be) → new_lookup(Float(Neg(Succ(wy44)), Pos(wy450)), wy49, be)
new_lookup159(wy3000, wy400100, wy401, wy41, Succ(wy2380), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup157(wy44, Pos(Succ(wy4500)), wy46, Neg(Zero), wy48, wy49, Succ(wy2290), be) → new_lookup(Float(Neg(Succ(wy44)), Pos(Succ(wy4500))), wy49, be)
new_lookup154(wy400100, wy401, wy41, Succ(wy2210), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup1117(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy22900), Succ(Succ(wy26000)), be) → new_lookup1125(wy44, wy4500, wy46, wy4700, wy48, wy49, wy22900, wy26000, be)
new_lookup182(wy51, Pos(Zero), wy53, Pos(Succ(wy5400)), wy55, wy56, Succ(wy3180), bf) → new_lookup0(Float(Neg(Succ(wy51)), Pos(Zero)), wy53, wy5400, wy55, wy56, bf)
new_lookup132(wy29, Pos(Zero), wy31, Neg(Succ(wy3200)), wy33, wy34, Succ(wy1380), bc) → new_lookup(Float(Pos(Succ(wy29)), Pos(Zero)), wy34, bc)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup176(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1128(wy51, wy5200, wy53, wy5400, wy55, wy56, wy3180, Zero, bf) → new_lookup0(Float(Neg(Succ(wy51)), Pos(Succ(wy5200))), wy53, wy5400, wy55, wy56, bf)
new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup178(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup112(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy660), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup1127(wy44, wy450, wy46, wy470, wy48, wy49, be) → new_lookup(Float(Neg(Succ(wy44)), Neg(wy450)), wy49, be)
new_lookup11(wy22, wy2300, wy24, wy2500, wy26, wy27, wy630, Zero, ba) → new_lookup(Float(Pos(Succ(wy22)), Neg(Succ(wy2300))), wy27, ba)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup145(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1(wy22, Neg(Zero), wy24, Neg(Succ(wy2500)), wy26, wy27, Succ(wy630), ba) → new_lookup(Float(Pos(Succ(wy22)), Neg(Zero)), wy27, ba)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup128(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup147(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1128(wy51, wy5200, wy53, wy5400, wy55, wy56, Zero, Succ(Succ(wy34900)), bf) → new_lookup1135(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup1(wy22, Neg(Succ(wy2300)), wy24, Pos(Succ(wy2500)), wy26, wy27, Zero, ba) → new_lookup14(wy22, wy2300, wy24, wy2500, wy26, wy27, new_primPlusNat0(new_primMulNat0(wy2300, wy2500), Succ(wy2500)), ba)
new_lookup11(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy6300), Succ(Succ(wy9000)), ba) → new_lookup1144(wy22, wy2300, wy24, wy2500, wy26, wy27, wy6300, wy9000, ba)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup181(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup172(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup182(wy51, Neg(wy520), wy53, Pos(wy540), wy55, wy56, Succ(wy3180), bf) → new_lookup(Float(Neg(Succ(wy51)), Neg(wy520)), wy56, bf)
new_lookup115(wy3000, wy400100, wy401, wy41, Succ(wy760), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup1144(wy22, wy2300, wy24, wy2500, wy26, wy27, Zero, Succ(wy9000), ba) → new_lookup1145(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup1144(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy6300), Zero, ba) → new_lookup1145(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup1133(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy3590), bf) → new_lookup1139(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup118(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup182(wy51, Neg(Zero), wy53, Neg(Succ(wy5400)), wy55, wy56, Succ(wy3180), bf) → new_lookup(Float(Neg(Succ(wy51)), Neg(Zero)), wy56, bf)
new_lookup164(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy2520), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup1113(wy29, wy3000, wy31, wy3200, wy33, wy34, Zero, Succ(wy17100), bc) → new_lookup1114(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup1113(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy13800), Zero, bc) → new_lookup1114(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup17(wy22, wy2300, wy24, wy2500, wy26, wy27, ba) → new_lookup(Float(Pos(Succ(wy22)), Pos(Succ(wy2300))), wy27, ba)
new_lookup157(wy44, Neg(wy450), wy46, Neg(wy470), wy48, wy49, Succ(wy2290), be) → new_lookup(Float(Neg(Succ(wy44)), Neg(wy450)), wy49, be)
new_lookup1104(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy13800), Succ(Succ(wy16900)), bc) → new_lookup1111(wy29, wy3000, wy31, wy3200, wy33, wy34, wy13800, wy16900, bc)
new_lookup121(wy400000, wy400100, wy401, wy41, Succ(wy1060), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup166(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy2700), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup138(wy3000, wy400100, wy401, wy41, Succ(wy1610), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup1136(wy51, wy520, wy53, wy540, wy55, wy56, bf) → new_lookup(Float(Neg(Succ(wy51)), Pos(wy520)), wy56, bf)
new_lookup114(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy720), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup185(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1(wy22, Pos(Succ(wy2300)), wy24, Pos(Succ(wy2500)), wy26, wy27, Succ(wy630), ba) → new_lookup10(wy22, wy2300, wy24, wy2500, wy26, wy27, wy630, new_primPlusNat0(new_primMulNat0(wy2300, wy2500), Succ(wy2500)), ba)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup1102(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup182(wy51, Neg(Succ(wy5200)), wy53, Neg(Zero), wy55, wy56, Succ(wy3180), bf) → new_lookup(Float(Neg(Succ(wy51)), Neg(Succ(wy5200))), wy56, bf)
new_lookup152(wy400100, wy401, wy41, Succ(wy2150), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup132(wy29, Neg(Succ(wy3000)), wy31, Pos(Zero), wy33, wy34, Succ(wy1380), bc) → new_lookup(Float(Pos(Succ(wy29)), Neg(Succ(wy3000))), wy34, bc)
new_lookup1129(wy51, wy5200, wy53, wy5400, wy55, wy56, Zero, Succ(Succ(wy35100)), bf) → new_lookup1139(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Zero))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup114(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup132(wy29, Neg(Succ(wy3000)), wy31, Pos(Succ(wy3200)), wy33, wy34, Zero, bc) → new_lookup1108(wy29, wy3000, wy31, wy3200, wy33, wy34, new_primPlusNat0(new_primMulNat0(wy3000, wy3200), Succ(wy3200)), bc)
new_lookup11(wy22, wy2300, wy24, wy2500, wy26, wy27, Zero, Succ(Succ(wy9000)), ba) → new_lookup1145(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup157(wy44, Neg(Succ(wy4500)), wy46, Pos(Zero), wy48, wy49, Succ(wy2290), be) → new_lookup(Float(Neg(Succ(wy44)), Neg(Succ(wy4500))), wy49, be)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup119(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup140(wy3000, wy400100, wy401, wy41, Succ(wy1670), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup125(wy400100, wy401, wy41, Succ(wy1180), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup177(wy400100, wy401, wy41, Succ(wy3040), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup132(wy29, Neg(Succ(wy3000)), wy31, Neg(Succ(wy3200)), wy33, wy34, Zero, bc) → new_lookup1109(wy29, wy3000, wy31, wy3200, wy33, wy34, new_primPlusNat0(new_primMulNat0(wy3000, wy3200), Succ(wy3200)), bc)
new_lookup168(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy2760), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup182(wy51, Pos(Succ(wy5200)), wy53, Pos(Succ(wy5400)), wy55, wy56, Zero, bf) → new_lookup1130(wy51, wy5200, wy53, wy5400, wy55, wy56, new_primPlusNat0(new_primMulNat0(wy5200, wy5400), Succ(wy5400)), bf)
new_lookup193(Succ(wy160), wy17, wy18, wy19, wy20, bg) → new_lookup1140(wy160, wy17, wy18, wy19, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy160, wy20), Succ(wy20)), Succ(wy20)), Succ(wy20)), bg)
new_lookup157(wy44, Pos(Succ(wy4500)), wy46, Pos(Succ(wy4700)), wy48, wy49, Zero, be) → new_lookup1118(wy44, wy4500, wy46, wy4700, wy48, wy49, new_primPlusNat0(new_primMulNat0(wy4500, wy4700), Succ(wy4700)), be)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup1103(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup188(wy3000, wy400100, wy401, wy41, Succ(wy3410), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup132(wy29, Pos(Succ(wy3000)), wy31, Neg(Zero), wy33, wy34, Succ(wy1380), bc) → new_lookup(Float(Pos(Succ(wy29)), Pos(Succ(wy3000))), wy34, bc)
new_lookup179(wy400100, wy401, wy41, Succ(wy3100), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup1105(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy13800), Succ(Zero), bc) → new_lookup1114(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup1107(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy1750), bc) → new_lookup1112(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup137(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy1570), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup126(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup182(wy51, Pos(wy520), wy53, Neg(wy540), wy55, wy56, Succ(wy3180), bf) → new_lookup(Float(Neg(Succ(wy51)), Pos(wy520)), wy56, bf)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup148(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup196(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy3730), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup1132(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy3570), bf) → new_lookup1137(wy51, Succ(wy5200), wy53, Succ(wy5400), wy55, wy56, bf)
new_lookup(Float(Neg(Succ(wy3000)), wy31), :(@2(Float(Neg(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup182(wy3000, wy31, wy400000, wy4001, wy401, wy41, new_primPlusNat0(new_primMulNat0(wy3000, wy400000), Succ(wy400000)), bb)
new_lookup1126(wy44, wy4500, wy46, wy4700, wy48, wy49, be) → new_lookup(Float(Neg(Succ(wy44)), Neg(Succ(wy4500))), wy49, be)
new_lookup165(wy3000, wy400100, wy401, wy41, Succ(wy2560), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup160(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup16(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy6300), Zero, ba) → new_lookup17(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup16(wy22, wy2300, wy24, wy2500, wy26, wy27, Zero, Succ(wy8800), ba) → new_lookup17(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup155(wy310000, wy400100, wy401, wy41, Succ(wy2230), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup163(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup184(wy3000, wy400100, wy401, wy41, Succ(wy3290), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup139(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy1630), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup18(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy3970), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup190(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup1101(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1(wy22, Neg(Succ(wy2300)), wy24, Neg(Succ(wy2500)), wy26, wy27, Succ(wy630), ba) → new_lookup11(wy22, wy2300, wy24, wy2500, wy26, wy27, wy630, new_primPlusNat0(new_primMulNat0(wy2300, wy2500), Succ(wy2500)), ba)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup167(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1103(wy400100, wy401, wy41, Succ(wy3950), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup1129(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy31800), Succ(Succ(wy35100)), bf) → new_lookup1138(wy51, wy5200, wy53, wy5400, wy55, wy56, wy31800, wy35100, bf)
new_lookup158(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy2340), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup112(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1105(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy13800), Succ(Succ(wy17100)), bc) → new_lookup1113(wy29, wy3000, wy31, wy3200, wy33, wy34, wy13800, wy17100, bc)
new_lookup1112(wy29, wy3000, wy31, wy3200, wy33, wy34, bc) → new_lookup(Float(Pos(Succ(wy29)), Pos(Succ(wy3000))), wy34, bc)
new_lookup182(wy51, Pos(Succ(wy5200)), wy53, Pos(Zero), wy55, wy56, Succ(wy3180), bf) → new_lookup(Float(Neg(Succ(wy51)), Pos(Succ(wy5200))), wy56, bf)
new_lookup136(wy3000, wy400100, wy401, wy41, Succ(wy1550), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup1119(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy2640), be) → new_lookup1124(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup1123(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy22900), Zero, be) → new_lookup1124(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup1123(wy44, wy4500, wy46, wy4700, wy48, wy49, Zero, Succ(wy25800), be) → new_lookup1124(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup1105(wy29, wy3000, wy31, wy3200, wy33, wy34, wy1380, Zero, bc) → new_lookup0(Float(Pos(Succ(wy29)), Neg(Succ(wy3000))), wy31, wy3200, wy33, wy34, bc)
new_lookup120(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy1020), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup1(wy22, Pos(Succ(wy2300)), wy24, Pos(Succ(wy2500)), wy26, wy27, Zero, ba) → new_lookup12(wy22, wy2300, wy24, wy2500, wy26, wy27, new_primPlusNat0(new_primMulNat0(wy2300, wy2500), Succ(wy2500)), ba)
new_lookup157(wy44, Neg(Succ(wy4500)), wy46, Pos(Succ(wy4700)), wy48, wy49, Zero, be) → new_lookup1120(wy44, wy4500, wy46, wy4700, wy48, wy49, new_primPlusNat0(new_primMulNat0(wy4500, wy4700), Succ(wy4700)), be)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup146(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup120(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup131(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup130(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup144(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1110(wy29, wy300, wy31, wy320, wy33, wy34, bc) → new_lookup(Float(Pos(Succ(wy29)), Pos(wy300)), wy34, bc)
new_lookup1134(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy31800), Zero, bf) → new_lookup1135(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup1134(wy51, wy5200, wy53, wy5400, wy55, wy56, Zero, Succ(wy34900), bf) → new_lookup1135(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup14(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy960), ba) → new_lookup1143(wy22, Succ(wy2300), wy24, Succ(wy2500), wy26, wy27, ba)
new_lookup1134(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy31800), Succ(wy34900), bf) → new_lookup1134(wy51, wy5200, wy53, wy5400, wy55, wy56, wy31800, wy34900, bf)
new_lookup182(wy51, Neg(Succ(wy5200)), wy53, Neg(Succ(wy5400)), wy55, wy56, Zero, bf) → new_lookup1133(wy51, wy5200, wy53, wy5400, wy55, wy56, new_primPlusNat0(new_primMulNat0(wy5200, wy5400), Succ(wy5400)), bf)
new_lookup173(wy400000, wy400100, wy401, wy41, Succ(wy2920), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup123(wy400000, wy400100, wy401, wy41, Succ(wy1120), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup173(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup124(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup146(wy400000, wy400100, wy401, wy41, Succ(wy1970), bb) → new_lookup0(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wy400000, wy400100, wy401, wy41, bb)
new_lookup172(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy2880), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup198(wy310000, wy400100, wy401, wy41, Succ(wy3790), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Zero))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup141(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(wy31000)))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup193(wy31000, Float(Neg(Zero), Neg(Succ(wy400100))), wy401, wy41, wy400100, bb)
new_lookup148(wy400000, wy400100, wy401, wy41, Succ(wy2030), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup183(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy3250), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup167(wy400000, wy400100, wy401, wy41, Succ(wy2740), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup16(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy6300), Succ(wy8800), ba) → new_lookup16(wy22, wy2300, wy24, wy2500, wy26, wy27, wy6300, wy8800, ba)
new_lookup174(wy310000, wy400100, wy401, wy41, Succ(wy2940), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup10(wy22, wy2300, wy24, wy2500, wy26, wy27, wy630, Zero, ba) → new_lookup(Float(Pos(Succ(wy22)), Pos(Succ(wy2300))), wy27, ba)
new_lookup1124(wy44, wy4500, wy46, wy4700, wy48, wy49, be) → new_lookup(Float(Neg(Succ(wy44)), Pos(Succ(wy4500))), wy49, be)
new_lookup124(wy310000, wy400100, wy401, wy41, Succ(wy1140), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup1113(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy13800), Succ(wy17100), bc) → new_lookup1113(wy29, wy3000, wy31, wy3200, wy33, wy34, wy13800, wy17100, bc)
new_lookup(Float(Pos(Succ(wy3000)), wy31), :(@2(Float(Pos(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup1(wy3000, wy31, wy400000, wy4001, wy401, wy41, new_primPlusNat1(new_primMulNat0(wy3000, wy400000), wy400000), bb)
new_lookup145(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy1930), bb) → new_lookup0(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy400000, wy400100, wy401, wy41, bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup116(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup10(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy6300), Succ(Zero), ba) → new_lookup17(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup134(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup127(wy400100, wy401, wy41, Succ(wy1240), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup116(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy780), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup161(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Zero))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Zero))), wy41, bb)
new_lookup133(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy1450), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup157(wy44, Neg(Succ(wy4500)), wy46, Neg(Succ(wy4700)), wy48, wy49, Zero, be) → new_lookup1121(wy44, wy4500, wy46, wy4700, wy48, wy49, new_primPlusNat0(new_primMulNat0(wy4500, wy4700), Succ(wy4700)), be)
new_lookup1128(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy31800), Succ(Succ(wy34900)), bf) → new_lookup1134(wy51, wy5200, wy53, wy5400, wy55, wy56, wy31800, wy34900, bf)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup191(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1138(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy31800), Succ(wy35100), bf) → new_lookup1138(wy51, wy5200, wy53, wy5400, wy55, wy56, wy31800, wy35100, bf)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup139(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1115(wy29, wy300, wy31, wy320, wy33, wy34, bc) → new_lookup(Float(Pos(Succ(wy29)), Neg(wy300)), wy34, bc)
new_lookup141(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy1810), bb) → new_lookup0(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy400000, wy400100, wy401, wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup195(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup153(wy310000, wy400100, wy401, wy41, Succ(wy2170), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup194(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy3670), bb) → new_lookup0(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy400000, wy400100, wy401, wy41, bb)
new_lookup1129(wy51, wy5200, wy53, wy5400, wy55, wy56, wy3180, Zero, bf) → new_lookup(Float(Neg(Succ(wy51)), Neg(Succ(wy5200))), wy56, bf)
new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup150(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), :(@2(Float(Neg(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup19(wy3000, wy400100, wy401, wy41, Succ(wy4000), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup192(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup189(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy3430), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup10(wy22, wy2300, wy24, wy2500, wy26, wy27, Zero, Succ(Succ(wy8800)), ba) → new_lookup17(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Zero))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Zero))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Zero))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Zero))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Zero))), wy41, bb)
new_lookup1(wy22, Neg(wy230), wy24, Pos(wy250), wy26, wy27, Succ(wy630), ba) → new_lookup(Float(Pos(Succ(wy22)), Neg(wy230)), wy27, ba)
new_lookup1128(wy51, wy5200, wy53, wy5400, wy55, wy56, Succ(wy31800), Succ(Zero), bf) → new_lookup1135(wy51, wy5200, wy53, wy5400, wy55, wy56, bf)
new_lookup1(wy22, Neg(Succ(wy2300)), wy24, Neg(Zero), wy26, wy27, Succ(wy630), ba) → new_lookup(Float(Pos(Succ(wy22)), Neg(Succ(wy2300))), wy27, ba)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup153(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup165(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup154(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup157(wy44, Pos(Zero), wy46, Neg(Zero), wy48, wy49, Succ(wy2290), be) → new_lookup(Float(Neg(Succ(wy44)), Pos(Zero)), wy49, be)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup129(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup191(wy310000, wy400000, wy400100, wy401, wy41, Succ(wy3610), bb) → new_lookup0(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy400000, wy400100, wy401, wy41, bb)
new_lookup1(wy22, Pos(Succ(wy2300)), wy24, Neg(Succ(wy2500)), wy26, wy27, Zero, ba) → new_lookup13(wy22, wy2300, wy24, wy2500, wy26, wy27, new_primPlusNat0(new_primMulNat0(wy2300, wy2500), Succ(wy2500)), ba)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup113(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup195(wy400000, wy400100, wy401, wy41, Succ(wy3710), bb) → new_lookup0(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wy400000, wy400100, wy401, wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup140(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup18(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup117(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup117(wy400000, wy400100, wy401, wy41, Succ(wy820), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup0(Float(Pos(Zero), Pos(Succ(Zero))), wy400000, wy400100, wy401, wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup0(Float(Neg(Zero), Neg(Succ(Zero))), wy400000, wy400100, wy401, wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Zero))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Zero))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Zero))), wy41, bb)
new_lookup186(wy3000, wy400100, wy401, wy41, Succ(wy3350), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup1(wy22, Neg(Zero), wy24, Neg(Zero), wy26, wy27, Succ(wy630), ba) → new_lookup(Float(Pos(Succ(wy22)), Neg(Zero)), wy27, ba)
new_lookup144(wy400000, wy400100, wy401, wy41, Succ(wy1910), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup1117(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy22900), Succ(Zero), be) → new_lookup1126(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup175(wy400100, wy401, wy41, Succ(wy2980), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup132(wy29, Neg(Zero), wy31, Pos(Zero), wy33, wy34, Succ(wy1380), bc) → new_lookup(Float(Pos(Succ(wy29)), Neg(Zero)), wy34, bc)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup174(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup142(wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup182(wy51, Pos(Succ(wy5200)), wy53, Neg(Succ(wy5400)), wy55, wy56, Zero, bf) → new_lookup1131(wy51, wy5200, wy53, wy5400, wy55, wy56, new_primPlusNat0(new_primMulNat0(wy5200, wy5400), Succ(wy5400)), bf)
new_lookup197(wy400000, wy400100, wy401, wy41, Succ(wy3770), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup194(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup0(wy411, wy412, wy413, wy414, wy415, bd) → new_lookup(wy411, wy415, bd)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup19(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup131(wy400100, wy401, wy41, Succ(wy1360), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup132(wy29, Neg(Zero), wy31, Pos(Succ(wy3200)), wy33, wy34, Succ(wy1380), bc) → new_lookup0(Float(Pos(Succ(wy29)), Neg(Zero)), wy31, wy3200, wy33, wy34, bc)
new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup149(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup129(wy400100, wy401, wy41, Succ(wy1300), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup198(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup115(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup10(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy6300), Succ(Succ(wy8800)), ba) → new_lookup16(wy22, wy2300, wy24, wy2500, wy26, wy27, wy6300, wy8800, ba)
new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup155(wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1125(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy22900), Zero, be) → new_lookup1126(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup1125(wy44, wy4500, wy46, wy4700, wy48, wy49, Zero, Succ(wy26000), be) → new_lookup1126(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup132(wy29, Pos(wy300), wy31, Pos(wy320), wy33, wy34, Succ(wy1380), bc) → new_lookup(Float(Pos(Succ(wy29)), Pos(wy300)), wy34, bc)
new_lookup157(wy44, Neg(Zero), wy46, Pos(Zero), wy48, wy49, Succ(wy2290), be) → new_lookup(Float(Neg(Succ(wy44)), Neg(Zero)), wy49, be)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Zero))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Zero))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup110(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1108(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy1770), bc) → new_lookup1114(wy29, wy3000, wy31, wy3200, wy33, wy34, bc)
new_lookup1109(wy29, wy3000, wy31, wy3200, wy33, wy34, Succ(wy1790), bc) → new_lookup1115(wy29, Succ(wy3000), wy31, Succ(wy3200), wy33, wy34, bc)
new_lookup176(wy310000, wy400100, wy401, wy41, Succ(wy3000), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup171(wy400000, wy400100, wy401, wy41, Succ(wy2860), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup150(wy400100, wy401, wy41, Succ(wy2090), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup1116(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy22900), Succ(Zero), be) → new_lookup1124(wy44, wy4500, wy46, wy4700, wy48, wy49, be)
new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), :(@2(Float(Pos(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup138(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Pos(Zero), Pos(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup179(wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup157(wy44, Pos(Succ(wy4500)), wy46, Neg(Succ(wy4700)), wy48, wy49, Zero, be) → new_lookup1119(wy44, wy4500, wy46, wy4700, wy48, wy49, new_primPlusNat0(new_primMulNat0(wy4500, wy4700), Succ(wy4700)), be)
new_lookup130(wy310000, wy400100, wy401, wy41, Succ(wy1320), bb) → new_lookup(Float(Pos(Zero), Neg(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup(Float(Neg(Zero), Neg(Succ(Zero))), wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Zero)))), :(@2(Float(Neg(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup188(wy3000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Zero))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup0(Float(Neg(Zero), Pos(Succ(Zero))), wy400000, wy400100, wy401, wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup166(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup(Float(Pos(Zero), Neg(Succ(Zero))), :(@2(Float(Neg(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup0(Float(Pos(Zero), Neg(Succ(Zero))), wy400000, wy400100, wy401, wy41, bb)
new_lookup(Float(Neg(Succ(wy3000)), wy31), :(@2(Float(Pos(Succ(wy400000)), wy4001), wy401), wy41), bb) → new_lookup157(wy3000, wy31, wy400000, wy4001, wy401, wy41, new_primPlusNat0(new_primMulNat0(wy3000, wy400000), Succ(wy400000)), bb)
new_lookup132(wy29, Neg(Succ(wy3000)), wy31, Pos(Succ(wy3200)), wy33, wy34, Succ(wy1380), bc) → new_lookup1105(wy29, wy3000, wy31, wy3200, wy33, wy34, wy1380, new_primPlusNat0(new_primMulNat0(wy3000, wy3200), Succ(wy3200)), bc)
new_lookup1143(wy22, wy230, wy24, wy250, wy26, wy27, ba) → new_lookup(Float(Pos(Succ(wy22)), Neg(wy230)), wy27, ba)
new_lookup110(wy3000, wy310000, wy400100, wy401, wy41, Succ(wy4010), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), wy41, bb)
new_lookup142(wy400000, wy400100, wy401, wy41, Succ(wy1850), bb) → new_lookup0(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), wy400000, wy400100, wy401, wy41, bb)
new_lookup(Float(Neg(Zero), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Succ(wy400000)), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup168(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup134(wy3000, wy400100, wy401, wy41, Succ(wy1490), bb) → new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Zero)))), wy41, bb)
new_lookup1122(wy44, wy450, wy46, wy470, wy48, wy49, be) → new_lookup(Float(Neg(Succ(wy44)), Pos(wy450)), wy49, be)
new_lookup(Float(Pos(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Neg(Zero), Neg(Succ(wy400100))), wy401), wy41), bb) → new_lookup135(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup1135(wy51, wy5200, wy53, wy5400, wy55, wy56, bf) → new_lookup0(Float(Neg(Succ(wy51)), Pos(Succ(wy5200))), wy53, wy5400, wy55, wy56, bf)
new_lookup(Float(Neg(Zero), Neg(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Succ(wy400000)), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup170(wy310000, wy400000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup163(wy3000, wy400100, wy401, wy41, Succ(wy2500), bb) → new_lookup(Float(Neg(Succ(wy3000)), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup1117(wy44, wy4500, wy46, wy4700, wy48, wy49, wy2290, Zero, be) → new_lookup(Float(Neg(Succ(wy44)), Neg(Succ(wy4500))), wy49, be)
new_lookup113(wy3000, wy400100, wy401, wy41, Succ(wy700), bb) → new_lookup(Float(Pos(Succ(wy3000)), Neg(Succ(Succ(Zero)))), wy41, bb)
new_lookup1104(wy29, wy3000, wy31, wy3200, wy33, wy34, wy1380, Zero, bc) → new_lookup(Float(Pos(Succ(wy29)), Pos(Succ(wy3000))), wy34, bc)
new_lookup12(wy22, wy2300, wy24, wy2500, wy26, wy27, Succ(wy920), ba) → new_lookup17(wy22, wy2300, wy24, wy2500, wy26, wy27, ba)
new_lookup1116(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy22900), Succ(Succ(wy25800)), be) → new_lookup1123(wy44, wy4500, wy46, wy4700, wy48, wy49, wy22900, wy25800, be)
new_lookup1(wy22, Pos(Zero), wy24, Pos(Zero), wy26, wy27, Succ(wy630), ba) → new_lookup(Float(Pos(Succ(wy22)), Pos(Zero)), wy27, ba)
new_lookup1123(wy44, wy4500, wy46, wy4700, wy48, wy49, Succ(wy22900), Succ(wy25800), be) → new_lookup1123(wy44, wy4500, wy46, wy4700, wy48, wy49, wy22900, wy25800, be)
new_lookup(Float(Neg(Succ(wy3000)), Pos(Succ(Succ(Succ(wy310000))))), :(@2(Float(Pos(Zero), Pos(Succ(wy400100))), wy401), wy41), bb) → new_lookup158(wy3000, wy310000, wy400100, wy401, wy41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat0(wy310000, wy400100), Succ(wy400100)), Succ(wy400100)), Succ(wy400100)), bb)
new_lookup193(Zero, wy17, wy18, wy19, wy20, bg) → new_lookup1141(wy17, wy18, wy19, new_primPlusNat0(new_primPlusNat0(Zero, Succ(wy20)), Succ(wy20)), bg)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, wy400000) → Succ(wy400000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy620), wy400000) → Succ(Succ(new_primPlusNat0(wy620, wy400000)))
new_primMulNat0(Zero, wy400000) → Zero
new_primPlusNat0(Succ(wy6200), Zero) → Succ(wy6200)
new_primPlusNat0(Zero, Succ(wy4000000)) → Succ(wy4000000)
new_primPlusNat0(Succ(wy6200), Succ(wy4000000)) → Succ(Succ(new_primPlusNat0(wy6200, wy4000000)))
new_primMulNat0(Succ(wy30000), wy400000) → new_primPlusNat1(new_primMulNat0(wy30000, wy400000), wy400000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, x0)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Succ(x0))
new_primMulNat0(Succ(x0), x1)
new_primPlusNat1(Zero, x0)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: